i, j:. ((i = j) ~ tt)  (i = j) 

latex

ProofTree

Definitions	t  T, x:A. B(x), P  Q, , P & Q, P  Q
Lemmas	int sq, btrue wf, assert of eq int, eqtt to assert, assert wf, bool wf, iff transitivity